:- module(abc_semantics, [
						  trans/2,
						  validate_instance/1,
						  start_state/2,
						  verify_ap/2,
						  state_label/2,
						  transition_system_def/2,
						  sem_start/1,
						  sem_start/2,
                          exec/1,
				          pred/2
						 ]).

:- use_module(library(lists)).
:- use_module(library(charsio)).
:- use_module(abc_parser).
:- use_module(avm_objects).


% =============================================================================
% #region Hooks for the model checker (temporary - FIXME)

% The model checker is expecting verify_ap, so just have verify_ap be a
% forwarding alias for pred
% TODO: Fix the discrepancy.
verify_ap(State, AP) :- pred(AP, State).


% `start_state` is a map between a TS and the actual start state. Since we have
% locked down the transition instance to a single file, this just accepts any
% name and returns the state created by `start`.
%start_state(Filename, S) :- sem_start(Filename, S).
start_state(_, S) :- sem_start(S).


% We currently do no (real) validation of the instance; we just parse the file
% and take it as-is. So just supply a dummy "sure everything's good"
% `validate_instance`.
%
% TODO (much later): write a real predicate to perform this task
validate_instance(_).


% A dummy transition_system_def - we don't actually have a transition system
% to use, though later on we'll want to map from this name to the parser.
% TODO: Map from the name provided to a filename that we send to the parser.
transition_system_def(_, none).


% The state label predicate (taken from the `exec` predicate below); prints
% out the environment and the instruction.
state_label(State, Label) :-
	State = state(_H, [Env | _R]),
	Env = env(_SS, _OS, _RF, Instr),
	get_property(Instr, label, InstrName),
	format_to_chars('Env: ~w | Instr: ~w', [Env, InstrName], Str),
	atom_chars(Label, Str).

state_label(halted, 'halted').

/**
 * Method for testing execution
 */

test(I) :-
	sem_start(S),!,
	test_helper(S,0,I),
	format('Done~n',[]).

test_helper(S,D,[readByte|Rest]) :-
	S = state(_H,[Env|_R]),
	Env = env(_SS,_OS,_RF,Instr),
	get_property(Instr,label,InstrName),
	pred(callpropvoid(readByte,_Args),S),
	print_tabs(D),
	format('readByte: ~w~n',[InstrName]),
	trans(S,NewS),
	NewD is D+1,
	test_helper(NewS,NewD,Rest).
test_helper(S,D,[writeByte|Rest]) :-
	S = state(_H,[Env|_R]),
	Env = env(_SS,_OS,_RF,Instr),
	get_property(Instr,label,InstrName),
	pred(callpropvoid(writeByte,_Args),S),
	print_tabs(D),
	format('writeByte: ~w~n',[InstrName]),
	trans(S,NewS),
	NewD is D+1,
	test_helper(NewS,NewD,Rest).
test_helper(S,D,[InstrName|Rest]) :-
	S = state(_H,[Env|_R]),
	Env = env(_SS,_OS,_RF,Instr),
	get_property(Instr,label,InstrName),
	\+pred(callpropvoid(writeByte,_Args),S),
	\+pred(callpropvoid(readByte,_Args),S),
	print_tabs(D),
	format('~w~n',[InstrName]),
	trans(S,NewS),
	NewD is D+1,
	test_helper(NewS,NewD,Rest).
test_helper(halted,_D,[]) :- format('Halted~n',[]).

print_tabs(0).
print_tabs(N) :-
	N > 0,
	format('~t',[]),
	NewN is N-1,
	print_tabs(NewN).


exec(E) :-
	sem_start(S),!,
	S = state(_H,[Env|_R]),
	Env = env(_SS,_OS,_RF,Instr),
	get_property(Instr,label,InstrName),
	format('Env: ~w~nInstr: ~w~n', [Env,InstrName]),
	exec_helper(S,[Env],E).

exec_helper(S,List,List) :-
	trans(S,halted),
	format('Halted~n~n', []).
exec_helper(S,Prev,List) :-
	trans(S,NewS),
	%pred(callpropvoid(connect,[string('example.com'),int(1234)]),NewS),
	pred(callpropvoid(readByte,_Args),NewS),
	NewS = state(_H,[Env|_R]),
	Env = env(_SS,_OS,_RF,Instr),
	append(Prev,[Env],Next),
	get_property(Instr,label,InstrName),
	format('Env: ~w~nInstr: ~w~ncallpropvoid matched!~n', [Env,InstrName]),
	exec_helper(NewS,Next,List).
exec_helper(S,Prev,List) :-
	trans(S,NewS),
	%\+pred(callpropvoid(connect,[string('example.com'),int(1234)]),NewS),
	\+pred(callpropvoid(readByte,_Args),NewS),
	NewS = state(_H,[Env|_R]),
	Env = env(_SS,_OS,_RF,Instr),
	append(Prev,[Env],Next),
	get_property(Instr,label,InstrName),
	format('Env: ~w~nInstr: ~w~n', [Env,InstrName]),
	exec_helper(NewS,Next,List).


/**
 * The VM state consists of the _heap_ and the _execution stack_. The 
 * execution stack is a stack of _execution environments_, which each 
 * consist of:
 * 1) a scope stack,
 * 2) an operand stack, and
 * 3) a register file,
 * along with a program counter to indicate which instruction is to be
 * executed next.
 */
% state(Heap,[EE|EEs]).
% env([S|Ss],[O|Os],[R|Rs],PC).

/**
 * pred(Action,State) returns true if the security-relevant predicate
 * Action is true in State.
 */
% TODO: Finish defining pred.

% No security relevant predicates are true for the halted state.
pred(_Action,halted) :- fail.
pred(callproperty(String,Args),state(_H,[env(_SS,OS,_RF,Instr)|_EEs])) :-
	get_property(Instr,label,callproperty),
	get_property(Instr,args,[Name,ArgCount]),
	get_property(Name,data,Multiname),
	get_property(Multiname,name,StringObj),
	get_property(StringObj,str,String),
	length(Args,ArgCount),
	reverse(Args,RArgs),
	append(RArgs,_Rest,OS).
pred(callpropvoid(String,Args),state(_H,[env(_SS,OS,_RF,Instr)|_EEs])) :-
	get_property(Instr,label,callpropvoid),
	get_property(Instr,args,[Name,ArgCount]),
	get_property(Name,data,Multiname),
	get_property(Multiname,name,StringObj),
	get_property(StringObj,str,String),
	length(Args,ArgCount),
	reverse(Args,RArgs),
	append(RArgs,_Rest,OS).




/**
 * start(State) returns the starting state of the state machine
 * that the model checker will traverse.
 */
% TODO: Finish defining the start state.
/*start(state(H,[env(ScopeStack,OperandStack,RegisterFile,Instr)]) :-
	initialize_global_object(GlobalObject),
	ScopeStack = [GlobalObject],
	get_heap(H).
*/

sem_start(S) :-
	G = 'Target.abc',
	U = 'TargetUnsafe.abc',
	L = 'TargetLoop.abc',
	sem_start(L, S).

sem_start(Filename, state(H,[env(ScopeStack,OperandStack,RegisterFile,Instr)])) :-
	parseFile(Filename,ABCObject),
	/*get_property(ABCObject,scripts,Scripts),
	last(Scripts,ScriptObject),
	get_property(ScriptObject,init,Method),*/
	get_property(ABCObject,methods,Methods),
	nth0(1,Methods,Method), % Go directly to the interesting method
	get_property(Method,has_body,true),
	get_property(Method,local_count,Count),
	length(RegisterFile,Count),
	top_list(RegisterFile),
	ScopeStack = [],
	OperandStack = [],
	get_property(Method,code,[Instr|_Rest]),
	get_heap(H), !.

% Used to generate a list of tt values
top_list([tt|R]) :- top_list(R).
top_list([]).

/**
 * Initializes the global object where builtins reside
 */
initialize_global_object(GlobalObject) :-
	get_base_object(Object),
	clone_object(Object,GlobalObject),
	set_internal_property(GlobalObject,'[[Class]]','Global'),
	set_internal_property(GlobalObject,'[[Prototype]]',null),
	initialize_object_prototype(ObjectPrototype,ObjectConstructor),
	initialize_function_prototype(FunctionPrototype,ObjectPrototype,FunctionConstructor),
	initialize_array_prototype(ArrayPrototype,ObjectPrototype,ArrayConstructor),
	initialize_object_constructor(ObjectPrototype,ObjectConstructor,FunctionPrototype),
	initialize_function_constructor(FunctionPrototype,FunctionConstructor),
	initialize_array_constructor(ArrayPrototype,ArrayConstructor,FunctionPrototype),
	set_properties(GlobalObject,['Object'-ObjectConstructor,
								 'Function'-FunctionConstructor,
								 'Array'-ArrayConstructor]).

initialize_object_prototype(ObjectPrototype,ObjectConstructor) :-
	get_base_object(Object),
	clone_object(Object,ObjectPrototype),
	set_internal_property(ObjectPrototype,'[[Class]]','Object'),
	set_internal_property(ObjectPrototype,'[[Prototype]]',null),
	set_property(ObjectPrototype,constructor,ObjectConstructor).

initialize_function_prototype(FunctionPrototype,ObjectPrototype,FunctionConstructor) :-
	subclass_object(ObjectPrototype,'Function',FunctionPrototype),
	set_property(FunctionPrototype,constructor,FunctionConstructor).

initialize_array_prototype(ArrayPrototype,ObjectPrototype,ArrayConstructor) :-
	subclass_object(ObjectPrototype,'Array',ArrayPrototype),
	set_property(ArrayPrototype,constructor,ArrayConstructor),
	set_internal_property(ArrayPrototype,'[[Put]]',array_put),
	set_property(ArrayPrototype,length,int(0)).

initialize_object_constructor(ObjectPrototype,ObjectConstructor,FunctionPrototype) :-
	extend_object(FunctionPrototype,ObjectConstructor),
	set_property(ObjectConstructor,prototype,ObjectPrototype),
	set_internal_property(ObjectConstructor,'[[Construct]]',abc_semantics:construct_obj(ObjectPrototype)),
	set_internal_property(ObjectConstructor,'[[Call]]',abc_semantics:construct_obj(ObjectPrototype)).

initialize_function_constructor(FunctionPrototype,FunctionConstructor) :-
	extend_object(FunctionPrototype,FunctionConstructor),
	set_property(FunctionConstructor,prototype,FunctionPrototype),
	set_internal_property(FunctionConstructor,'[[Construct]]',abc_semantics:construct_fun),
	set_internal_property(FunctionConstructor,'[[Call]]',abc_semantics:construct_fun).

initialize_array_constructor(ArrayPrototype,ArrayConstructor,FunctionPrototype) :-
	extend_object(FunctionPrototype,ArrayConstructor),
	set_property(ArrayConstructor,prototype,FunctionPrototype),
	set_internal_property(ArrayConstructor,'[[Construct]]',abc_semantics:construct_array),
	set_internal_property(ArrayConstructor,'[[Call]]',abc_semantics:construct_array).

/**
 * Implementations of [[Construct]] and [[Call]] predicates. These require
 * knowledge of the state representation from the semantics file.
 */

construct_obj(ObjectPrototype,[],state(_H,[env(SS,OS,RF,Instr)|EEs]),state(NH,[env(SS,[NewObject|OS],RF,NewInstr)|EEs])) :-
	extend_object(ObjectPrototype,NewObject),
	get_property(Intsr,next,NewInstr),
	get_heap(NH).

construct_obj(ObjectPrototype,[ref(Ref)],state(H,[env(SS,OS,RF,Instr)|EEs]),state(H,[env(SS,[ref(Ref)|OS],RF,NewInstr)|EEs])) :-
	get_property(Instr,next,NewInstr).

construct_obj(ObjectPrototype,[Value],state(H,[env(SS,OS,RF,Instr)|EEs]),state(H,[env(SS,[tt|OS],RF,NewInstr)|EEs])) :-
	Value \= ref(_Ref),
	get_property(Instr,next,NewInstr).

construct_fun([Args],state(H,[env(SS,OS,RF,Instr)|EEs]),state(H,[env(SS,[tt|OS],RF,NewInstr)|EEs])) :-
	get_property(Instr,next,NewInstr).

/**
 * trans(State1,State2) executes the current instruction, moving the 
 * state of the virtual machine from State1 to State2. Note that transitions
 * are actually processed by the helper predicate instr/3--this is to
 * abstract the notion of instructions for the model checker's transition
 * system.
 */

% Once the virtual machine is halted, the state remains fixed.
trans(halted,halted).

% The next state after any instruction could be halted. This simulates
% that the power to the machine could be shut off, etc.
% This implies we can only enforce safety properties
trans(state(_H,[]),halted).

% If the virtual machine is not halted, lookup the current instruction
% and execute the instruction transition helper predicate.
trans(State1,State2) :-
	State1 \= halted,
	cur_instr(State1,Instr),
	instr(Instr,State1,State2).

% The next state after any instruction could be halted. This simulates
% that the power to the machine could be shut off, etc.
% This implies we can only enforce safety properties
trans(State1,halted) :-
	State1 \= halted.

/**
 * cur_instr(State1,Instr) returns the mnemonic of the current instruction,
 * to be used as a tag for the instr/3 predicate.
 */
cur_instr(state(_H,[env(_SS,_OS,_RF,Instr)|_EEs]),Tag) :-
	get_property(Instr,label,Tag).

/**
 * instr(Instr,State1,State2) executes the given instruction in the
 * context of State1, moving the virtual machine from State1 to State2
 */

instr(add_i,state(H,[EE|EEs]),state(H,[NewEE|EEs])) :-
	EE =.. [env, ScopeStack, [int(O1),int(O2)|Os], RegisterFile, Instr],
	Result is O1 + O2,
	get_property(Instr,next,NewInstr),
	NewEE =.. [env, ScopeStack, [int(Result)|Os], RegisterFile, NewInstr].
instr(add_i,state(H,[EE|EEs]),state(H,[NewEE|EEs])) :-
	EE =.. [env, ScopeStack, [O1,O2|Os], RegisterFile, Instr],
	\+defined([O1,O2]), % this is the case where at least one argument is top
	get_property(Instr,next,NewInstr),
	NewEE =.. [env, ScopeStack, [tt|Os], RegisterFile, NewInstr].

instr(callproperty, state(H, [EE|EEs]), state(H, [NewEE|EEs])) :- %TODO
	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr,next,NewInstr),
	get_property(Instr,args,[_Namespace,ArgCount]),
	length(ToPop,ArgCount+1),
	append(ToPop,Rest,OperandStack),
	NewEE =.. [env, ScopeStack, [tt|Rest], RegisterFile, NewInstr].

instr(callpropvoid, state(H, [EE|EEs]), state(H, [NewEE|EEs])) :- %TODO
	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr,next,NewInstr),
	get_property(Instr,args,[_Namespace,ArgCount]),
	length(ToPop,ArgCount+1),
	append(ToPop,Rest,OperandStack),
	NewEE =.. [env, ScopeStack, Rest, RegisterFile, NewInstr].

instr(coerce, state(H, [EE|EEs]), state(H, [NewEE|EEs])) :- % CORRECT FOR NOW
	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr,next,NewInstr),
	NewEE =.. [env, ScopeStack, OperandStack, RegisterFile, NewInstr].

instr(constructprop, state(H, [EE|EEs]), state(H, [NewEE|EEs])) :- %TODO
	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr,next,NewInstr),
	get_property(Instr,args,[_NameSpace,ArgCount]),
	length(ToPop,ArgCount+1),
	append(ToPop,Rest,OperandStack),
	NewEE =.. [env, ScopeStack, [tt|Rest], RegisterFile, NewInstr].

instr(constructsuper, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- %TODO
	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr,next,NewInstr),
	get_property(Instr,args,[ArgCount]),
	length(ToPop,ArgCount+1),
	append(ToPop,Rest,OperandStack),
	NewEE =.. [env, ScopeStack, Rest, RegisterFile, NewInstr].

instr(convert_i, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- 
	EE =.. [env, ScopeStack, [O|Os], RegisterFile, Instr],
	toInt(O,Result),
	get_property(Instr,next,NewInstr),
	NewEE =.. [env, ScopeStack, [Result|Os], RegisterFile, NewInstr].

% toInt converts from one of the types either specified in the ECMA 262 document
% or in the AVM 2 Overview Document, whichever one is more specific to an int.
% currently assumes that we are dealing only with integers. For the rest,
% returns top.
toInt(undefined, undefined).
toInt(null, null).
toInt(bool(true), int(1)).
toInt(bool(false), int(0)).
toInt(int(Value),int(Value)).
toInt(int32(Value),int(Value)).
toInt(uint32(Value), int(Value)).
toInt(uint16(Value),int(Value)).
toInt(double(Value),int(Value)).
toInt(string(Value),tt).
toInt(object(Value),tt).
toInt(reference(Value),tt).
toInt(list(Value),tt).
toInt(completion(Value),tt).
toInt(namespace(Value), NewVal) :- 
	toInt(Value, NewVal).

instr(dup, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- 
	EE =.. [env, ScopeStack, [O|Os], RegisterFile, Instr],
	get_property(Instr, next, NewInstr),	
   	NewEE =.. [env, ScopeStack, [O,O|Os], RegisterFile, NewInstr].	

instr(findproperty, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- true. %TODO

instr(findpropstrict, state(H, [EE|EEs]), state(H, [NewEE|EEs])):-
	EE =.. [env, ScopeStack, Os, RegisterFile, Instr],
	get_property(Instr, next, NewInstr),
	NewEE =.. [env, ScopeStack, [tt|Os], RegisterFile, NewInstr].

instr(getlex, state(H, [EE|EEs]), state(H, [NewEE|EEs])):-
	EE =.. [env, ScopeStack, Os, RegisterFile, Instr],
	get_property(Instr, next, NewInstr),
	NewEE =.. [env, ScopeStack, [tt|Os], RegisterFile, NewInstr].

instr(getlocal, state(H, [EE|EEs]), state(H, [NewEE|EEs]))  :-
	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr,args,[Index]),
	get_property(Instr,next,NewInstr),
	nth0(Index, RegisterFile, Data),
	NewEE =.. [env, ScopeStack, [Data|OperandStack], RegisterFile, NewInstr].
	
instr(getlocal_0, state(H, [EE|EEs]), state(H, [NewEE|EEs])) :-
   	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr, next, NewInstr),
	nth0(0, RegisterFile, Data),	
   	NewEE =.. [env, ScopeStack, [Data|OperandStack], RegisterFile, NewInstr].	
	
instr(getlocal_1, state(H, [EE|EEs]), state(H, [NewEE|EEs])) :-
   	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr, next, NewInstr),	
	nth0(1, RegisterFile, Data),
   	NewEE =.. [env, ScopeStack, [Data|OperandStack], RegisterFile, NewInstr].	
	
instr(getlocal_2, state(H, [EE|EEs]), state(H, [NewEE|EEs])) :-
   	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr, next, NewInstr),
	nth0(2, RegisterFile, Data),	
   	NewEE =.. [env, ScopeStack, [Data|OperandStack], RegisterFile, NewInstr].

instr(getlocal_3, state(H, [EE|EEs]), state(H, [NewEE|EEs])) :-
   	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr, next, NewInstr),
	nth0(3, RegisterFile, Data),	
   	NewEE =.. [env, ScopeStack, [Data|OperandStack], RegisterFile, NewInstr].

instr(getglobalscope, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- 
	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr, next, NewInstr),
	last(ScopeStack, GlobalScope),	
   	NewEE =.. [env, ScopeStack, [GlobalScope|OperandStack], RegisterFile, NewInstr].	

instr(getproperty, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- % TODO
	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr, next, NewInstr),
	NewEE =.. [env, ScopeStack, OperandStack, RegisterFile, NewInstr].

%Index must be between 0 and ScopeDepth-1. Assuming that the bytecode loader
%takes care of that.
instr(getscopeobject, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- 
	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr, next, NewInstr),
	get_property(Instr,args,[Index]),
	length(ScopeStack, ScopeDepth),
	NewIndex is (ScopeDepth - 1) - Index,
	nth0(NewIndex, ScopeStack, ScopeObject),	
   	NewEE =.. [env, ScopeStack, [ScopeObject|OperandStack], RegisterFile, NewInstr].	

instr(getslot, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- true. %TODO

instr(greaterequals, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- 
	EE =.. [env, ScopeStack, [V1,V2|Os], RegisterFile, Instr],
	get_property(Instr,next,NewInstr),
	isgreaterequals(V1, V2, TruthValue),
	NewEE =.. [env, ScopeStack, [TruthValue|Os], RegisterFile, NewInstr].
    
%isgreaterequals compares the first and the second parameters using the
%Abstract Relational Comparison Algorithm, as described in ECMA-262 section
%11.8.5. Returns true if V1 >= V2, false if V1 < V2, and truefalse if the
%truth value cannot be determined, or we don't care.
%
%Not implemented yet.
isgreaterequals(int(V1), int(V2), bool(true)) :- V1 >= V2.
isgreaterequals(int(V1), int(V2), bool(false)) :- V1 < V2.
isgreaterequals(V1, V2, tt) :-
	V1 \= int(_X); V2 \= int(_Y).

instr(ifeq, state(H, [EE|EEs]), state(H, [NewEE|EEs])) :-
	EE =.. [env, ScopeStack, [V1,V2|Os], RegisterFile, Instr],
	isequals(V1, V2, TruthValue),
	help_ifeq(TruthValue,Instr,NewInstr),
	NewEE =.. [env, ScopeStack, Os, RegisterFile, NewInstr].

isequals(int(V1), int(V1), bool(true)).
isequals(int(V1), int(V2), bool(false)) :- V1 =\= V2.
isequals(V1, V2, tt) :-
	V1 \= int(_X); V2 \= int(_Y).

help_ifeq(bool(true), Instr, NewInstr) :-
	get_property(Instr, jumplabel, NewInstr).
help_ifeq(bool(false), Instr, NewInstr) :-
	get_property(Instr, next, NewInstr).
help_ifeq(tt, Instr, NewInstr) :-
	get_property(Instr, jumplabel, NewInstr).
help_ifeq(tt, Instr, NewInstr) :-
	get_property(Instr, next, NewInstr).

instr(iflt, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- 
	EE =.. [env, ScopeStack, [V1,V2|Os], RegisterFile, Instr],
	isgreaterequals(V1, V2, TruthValue),
	help_iflt(TruthValue,Instr,NewInstr),
	NewEE =.. [env, ScopeStack, Os, RegisterFile, NewInstr].

help_iflt(bool(true), Instr, NewInstr) :- 
	get_property(Instr, next, NewInstr).
help_iflt(bool(false), Instr, NewInstr) :-
	get_property(Instr, jumplabel, NewInstr).
help_iflt(tt, Instr, NewInstr) :-
	get_property(Instr, next, NewInstr).
help_iflt(tt, Instr, NewInstr) :-
	get_property(Instr, jumplabel, NewInstr).

instr(ifngt, state(H, [EE|EEs]), state(H, [NewEE|EEs])) :-
	EE =.. [env, ScopeStack, [V1,V2|Os], RegisterFile, Instr],
	isgreaterequals(V2,V1,TruthValue),
	help_ifngt(TruthValue,Instr,NewInstr),
	NewEE =.. [env, ScopeStack, Os, RegisterFile, NewInstr].

help_ifngt(bool(true), Instr, NewInstr) :-
	get_property(Instr, jumplabel, NewInstr).
help_ifngt(bool(false), Instr, NewInstr) :-
	get_property(Instr, next, NewInstr).
help_ifngt(tt, Instr, NewInstr) :-
	get_property(Instr, next, NewInstr).
help_ifngt(tt, Instr, NewInstr) :-
	get_property(Instr, jumplabel, NewInstr).

instr(increment_i, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- 
	EE =.. [env, ScopeStack, [O|Os], RegisterFile, Instr],
	toInt(O,X),
	help_increment_i(X, NewVal),
	get_property(Instr, next, NewInstr),	
   	NewEE =.. [env, ScopeStack, [NewVal|Os], RegisterFile, NewInstr].

help_increment_i(int(R1), int(R2)) :- R2 is R1 + 1.
help_increment_i(_, tt).

instr(initproperty, state(H, [EE|EEs]), state(H, [NewEE|EEs])) :- true. % TODO

instr(jump, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- 
	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr,jumplabel,JumpInstr),
	NewEE =.. [env, ScopeStack, OperandStack, RegisterFile, JumpInstr].

instr(kill, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- 
	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr,args,[Index]),
	get_property(Instr,next,NewInstr),	
	replace(Index, RegisterFile, undefined, NewRegisterFile),
   	NewEE =.. [env, ScopeStack, OperandStack, NewRegisterFile, NewInstr].	

instr(label, state(H, [EE|EEs]), state(H, [NewEE|EEs])) :-
	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr,next,NewInstr),
	NewEE =.. [env, ScopeStack, OperandStack, RegisterFile, NewInstr].

instr(newclass, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- % TODO
	EE =.. [env, ScopeStack, [O|Os], RegisterFile, Instr],
	get_property(Instr, next, NewInstr),
	NewEE =.. [env, ScopeStack, [tt|Os], RegisterFile, NewInstr].

instr(pop, state(H, [EE|EEs]), state(H, [NewEE|EEs])) :-
	EE =.. [env, ScopeStack, [O|Os], RegisterFile, Instr],
	get_property(Instr,next,NewInstr),
	NewEE =.. [env, ScopeStack, Os, RegisterFile, NewInstr].

instr(popscope, state(H, [EE|EEs]), state(H, [NewEE|EEs])):-   
	EE =.. [env, [S|Ss], OperandStack, RegisterFile, Instr],
	get_property(Instr, next, NewInstr),	
   	NewEE =.. [env, Ss, OperandStack, RegisterFile, NewInstr].

instr(pushbyte, state(H, [EE|EEs]), state(H, [NewEE|EEs])):-
	EE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	get_property(Instr, next, NewInstr),
	get_property(Instr, args, [Byte]),
	NewEE =.. [env, ScopeStack, [int(Byte)|OperandStack], RegisterFile, NewInstr].

instr(pushscope, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- 
	EE =.. [env, ScopeStack, [O|Os], RegisterFile, Instr],
	get_property(Instr, next, NewInstr),	
   	NewEE =.. [env, [O|ScopeStack], Os, RegisterFile, NewInstr].

instr(pushshort, state(H, [EE|EEs]), state(H, [NewEE|EEs])) :-
	EE =.. [env, ScopeStack, Os, RegisterFile, Instr],
	get_property(Instr, next, NewInstr),
	get_property(Instr, args, [Short]),
   	NewEE =.. [env, ScopeStack, [int(Short)|Os], RegisterFile, NewInstr].

instr(pushstring, state(H, [EE|EEs]), state(H, [NewEE|EEs])) :-
	EE =.. [env, ScopeStack, Os, RegisterFile, Instr],
	get_property(Instr, next, NewInstr),
	get_property(Instr, args, [StringObj]),
	get_property(StringObj, str, Str),
   	NewEE =.. [env, ScopeStack, [string(Str)|Os], RegisterFile, NewInstr].

instr(returnvoid, state(H, [_EE,PEE|EEs]), state(H, [NewPEE|EEs])):-
	PEE =.. [env, ScopeStack, OperandStack, RegisterFile, Instr],
	NewPEE =.. [env, ScopeStack, [undefined|OperandStack], RegisterFile, Instr].

instr(returnvoid, state(H, [_EE]), halted).

instr(setlocal, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- 
 	EE =.. [env, ScopeStack, [O|Os], RegisterFile, Instr],
	get_property(Instr,args,[Index]),
	get_property(Instr,next,NewInstr),
	replace(Index, RegisterFile, O, NewRegisterFile),
	NewEE =.. [env, ScopeStack, Os, NewRegisterFile, NewInstr].

instr(setlocal_0, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- 
	EE =.. [env, ScopeStack, [O|Os], RegisterFile, Instr],
	get_property(Instr,next,NewInstr),
	replace(0, RegisterFile, O, NewRegisterFile),
	NewEE =.. [env, ScopeStack, Os, NewRegisterFile, NewInstr].

instr(setlocal_1, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- 
	EE =.. [env, ScopeStack, [O|Os], RegisterFile, Instr],
	get_property(Instr,next,NewInstr),
	replace(1, RegisterFile, O, NewRegisterFile),
	NewEE =.. [env, ScopeStack, Os, NewRegisterFile, NewInstr].

instr(setlocal_2, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- 
	EE =.. [env, ScopeStack, [O|Os], RegisterFile, Instr],
	get_property(Instr,next,NewInstr),
	replace(2, RegisterFile, O, NewRegisterFile),
	NewEE =.. [env, ScopeStack, Os, NewRegisterFile, NewInstr].

instr(setlocal_3, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- 
	EE =.. [env, ScopeStack, [O|Os], RegisterFile, Instr],
	get_property(Instr,next,NewInstr),
	replace(3, RegisterFile, O, NewRegisterFile),
	NewEE =.. [env, ScopeStack, Os, NewRegisterFile, NewInstr].

instr(setproperty, state(H, [EE|EEs]), state(H, [NewEE|EEs])):- true. %TODO







/**
 * defined/1 is true if the argument is not a list and not top (tt),
 * or true if the argument is either an empty list or a list where
 * every element satisfies defined/1.
 */
defined([]).
defined([H|R]) :- 
	H \= tt, 
	defined(R).

%helper function for replacing the nth element in a list with the given 
%element. Index starts at 0, so it is really the (n-1)th element that 
%is being replaced.
%
replace(Index, OrigList, NewVal, NewList) :-
	nth0(Index, OrigList, _, L2),
	nth0(Index, NewList, NewVal, L2).

